En la herramienta, el usuario indica la vista SQL de la que quiere obtener el caso de prueba así como el máximo número de filas del caso de prueba para cada tabla relacionada con dicha vista. A partir de estos datos, se genera una instancia simbólica de estas tablas (con variables simbólicas frescas para cada atributo de cada fila) a la que posteriormente se aplicarán las restricciones generadas para obtener, a través de la resolución de las mismas, una instancia concreta que represente un caso de prueba positivo de la vista objetivo.


Siguiendo la metodología propuesta en \cite{flops2010}\cite{prole2012}, para cierta instancia simbólica $d$ de la base de datos $D$, representamos las restricciones asociadas a cada relación (tabla o vista) $R$ como un multiconjuto $\theta(R,d)$ de pares $(\psi,u)$ donde $\psi$ es una fórmula de primer orden y $u$ una fila de dicha relación. Representamos estas filas como sustituciones de sus atributos por expresiones sobre variables simbólicas y constantes con la siguiente notación: $(R.A_1 \mapsto e_{1},\dots,R.A_m \mapsto e_{m})$, siendo $R.A_1 , \dots, R.A_m$ los atributos de la relación y $e_1, \dots, e_m$ expresiones de variables simbólicas y constantes. Definimos el multiconjunto $theta(R,d)$ como:

\begin{enumerate}
\item \label{def:constraints:table} Para cada tabla $T$ con atributos $T.C_1, \dots, T.C_m$ de $D$ creamos una instancia simbólica $d$ con filas $\mu_1, \dots , \mu_n$ (donde n es el número de filas especificado por el usuario) y donde cada fila $\mu_i$ está compuesta por variables simbólicas frescas $X_{ij}$ con j $\in 1 \dots m$, siendo el tipo de $X_{ij}$ igual al tipo del atributo $T.C_j$.
\begin{itemize}
\item  Si la definición de $T$ no tiene claves primarias (\cod{PRIMARY KEY}) ni ajenas (\cod{FOREIGN KEY}):
  $\theta(T,d) = \multi{ (true,\mu_1), \dots, (true,\mu_n) }$. Donde $true$ simboliza que no hay restricciones sobre las filas $\mu_i$.
\item \label{def:constraints:primary} Si $T$ tiene una clave primaria para las columnas $T.C_1, \dots, T.C_p $:
  Sea $T'$ la tabla $T$ sin dicha clave primaria.
  Supongamos que $\theta(T',d) = \multileft (\psi_1,\mu_1),$ $\dots,$ $(\psi_n,\mu_n) \multiright$, entonces $\theta(T,d)$ es igual a $$\multi{((\psi_i \wedge (\bigwedge_{j=1, j\neq i}^n(\bigvee_{k=1}^p \mu_i(T.C_k) \neq \mu_j(T.C_k) ))),\mu_i)|i \in 1,\dots,n}$$

\item \label{def:constraints:foreign} Si $T$ tiene una clave ajena para las columnas $T.C_1, \dots, T.C_f $ referenciando las columnas $T2.C'_1,...T2.C'_f$ de la tabla $T2$:
  Sea $T'$ la tabla $T$ sin la clave ajena.
  Supongamos que $\theta(T',d) = \multi{ (\psi_1,\mu_1), \dots, (\psi_n,\mu_n) }$ y que  $d(T_2) = \multi{\nu_1, \dots, \nu_{n'}}$, entonces $\theta(T,d)$ es igual a $$ \multi{((\psi_i \wedge (\bigvee_{j=1, j\neq i}^{n'}(\bigwedge_{k=1}^f \mu_i(T.C_k) = \nu_j(T2.C'_k) ))),\mu_i)|i \in 1,\dots,n}$$
\end{itemize}
\item \label{def:constraints:view} Para toda vista $V =$ {\sf create view} V($E_1$, \dots, $E_n$) {\sf as} $Q$,
     $$\theta(V,d) = \theta(Q,d)\{V.E_1 \mapsto Q.A_1, \dots, V.E_n\mapsto A_n   \}$$


\item \label{def:constraints:basic} Si $Q$ es una consulta básica de la forma:
$$
\begin{array}{rl}
  &\textrm{\sf select }e_1, \dots, e_n \  {\sf from }\ R_1\ B_1 , \dots, R_m \ B_m\  \textrm{\sf where}\ C_w;
\end{array}
$$
Entonces $\theta(Q,d)$ es igual a:
$$
   \begin{array}{ll}
   & \multileft{ (\psi_1 \wedge \dots \wedge \psi_m \wedge \ftx{C_w\mu}{d},\,s_Q(\mu))\ \mid } \\
   &\quad   (\psi_1, \nu_1) \in \theta(R_1,d), \dots, (\psi_m, \nu_m) \in \theta(R_m,d),  \mu = {\nu_1}^{B_1} \odot \cdots \odot {\nu_m}^{B_m}   \multiright
  \end{array}
$$
  donde
  \begin{itemize}
   \item  $\odot$ representa el operador de unión de filas.
   \item $s_Q(\mu)$ = $\{Q.A_1 \mapsto (e_1 \mu), \dots, Q.A_n \mapsto (e_n \mu) \}$,
   \item La fórmula de primer orden $\ftx{C}{d}$ se define como:
   \begin{itemize}
        \item Si $C \equiv \cod{false}$ entonces  $\ftx{C}{d} = \bot$
        \item Si $C \equiv \cod{true}$ entonces  $\ftx{C}{d} = \top$
        \item Si $C \equiv e$, con $e$ una expresión aritmética con constantes entonces:
              $\ftx{C}{d} = e$
        \item Si $C \equiv e_1 \diamond e_2$, con  $\diamond$ un operador relacional, entonces  $\ftx{C}{d} = (\ftx{e_1}{d} \diamond \ftx{e_2}{d})$ .
        \item Si $C \equiv C_1\ \cod{ and }\ C_2$ entonces $\ftx{C}{d} = \ftx{C_1}{d} \wedge \ftx{C_2}{d}$
        \item Si $C \equiv C_1\ \cod{ or }\ C_2$ entonces $\ftx{C}{d} =\ftx{C_1}{d} \vee \ftx{C_2}{d}$
        \item Si $C \equiv \cod{ not }\ C_1$ entonces $\ftx{C}{d} = \neg \ftx{C}{d}$
        \item Si $C \equiv \cod{ exists }\ Q$
        supongamos que
         $\theta(Q,d) = \multi{ (\psi_1, \mu_1), \dots (\psi_{p},\mu_{p}) }$.
     Entonces  $\ftx{C}{d} = (\vee_{j=1}^{p} \psi_j)$.

        \end{itemize}

 \end{itemize}
\item \label{def:constraints:set} Si $Q$ es una consulta con operaciones de conjuntos:
     \begin{itemize}
    \item  $ \theta(V_1 \ \textrm{\sf union }\ V_2,d) = \theta({V_1},d)\ \cup\ \theta({V_2},d)$
                siendo $\cup$ la unión de multiconjuntos.
    \item $(\psi,\mu) \in \theta(V_1\ \textrm{\sf intersection }\ V_2,d)$   con cardinal $k$ si y solo si
          $(\psi_1,\mu) \in \theta(V_1,d)$ con cardinal $k_1$, $(\psi_2,\mu) \in \theta(V_2,d)$
          con cardinal $k_2$, $k=min(k_1,k_2)$ y $\psi = \psi_1 \wedge \psi_2$.
    \end{itemize}


\end{enumerate}

Obsérvese que si una consulta tiene una sección select de la forma {\sf select $e_1$ $E_1$, \dots, $e_n$ $E_n$}, la notación $s_Q(x)$ refiere al resultado de reemplazar en x cada $E_i$ por su valor $e_i$.

Estas directrices se aplican para transformar la estructura generada en la fase de análisis sintáctico a partir la definición de la base de datos en las restricciones asociadas a sus relaciones para obtener un caso de prueba.

 
